1 /-
2 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Johannes Hölzl, Casper Putz
5
6 The equivalence between matrices and linear maps.
7 -/
8
9 import data.matrix.basic
src └───────────────┘
10 import linear_algebra.dimension linear_algebra.tensor_product
src └──────────────────────┘ └───────────────────────────┘
11
12 /-!
13
14 # Linear maps and matrices
15
16 This file defines the maps to send matrices to a linear map,
17 and to send linear maps between modules with a finite bases
18 to matrices. This defines a linear equivalence between linear maps
19 between finite-dimensional vector spaces and matrices indexed by
20 the respective bases.
21
22 Some results are proved about the linear map corresponding to a
23 diagonal matrix (range, ker and rank).
24
25 ## Main definitions
26
27 to_lin, to_matrix, linear_equiv_matrix
28
29 ## Tags
30
31 linear_map, matrix, linear_equiv, diagonal
32
33 -/
34
35 noncomputable theory
36
37 open set submodule
38
39 universes u v w
40 variables {l m n : Type u} [fintype l] [fintype m] [fintype n]
id └─────┘ └─────┘ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ └─────┘ └─────┘
doc └─────┘ └─────┘ └─────┘
41
42 namespace matrix
43
44 variables {R : Type v} [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
45 instance [decidable_eq m] [decidable_eq n] (R) [fintype R] : fintype (matrix m n R) :=
id └──────────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └─────┘ └────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └─────┘ └─────┘ └────┘
typ └──────────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └─────┘ └────┘ ┴ ┴ ┴
doc └─────┘ └─────┘
46 by unfold matrix; apply_instance
src └───────────┘ └──────────────
typ └───────────┘ └──────────────
doc └───────────┘ └──────────────
txt └───────────┘ └──────────────
par └───────────┘ └──────────────
pid └─────┘ └
st └──────────────────────────────
47
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
48 /-- Evaluation of matrices gives a linear map from matrix m n R to
49 linear maps (n → R) →ₗ[R] (m → R). -/
50 def eval : (matrix m n R) →ₗ[R] ((n → R) →ₗ[R] (m → R)) :=
51 begin
52 refine linear_map.mk₂ R mul_vec _ _ _ _,
src └─────┘ ┴ ┴ └──────┘
typ └─────┘ ┴ ┴ └──────┘
doc └─────┘ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
53 { assume M N v, funext x,
src └──────────┘ └──────┘
typ └──────────┘ └──────┘
doc └──────────┘ └──────┘
txt └──────────┘ └──────┘
par └──────────┘ └──────┘
pid └──────────┘ └┘
54 change finset.univ.sum (λy:n, (M x y + N x y) * v y) = _,
src └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
typ └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
doc └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
txt └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
par └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
pid ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
55 simp only [_root_.add_mul, finset.sum_add_distrib],
src └─────────┘ └┘ ┴
typ └─────────┘ └┘ ┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
56 refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
57 { assume c M v, funext x,
src └──────────┘ └──────┘
typ └──────────┘ └──────┘
doc └──────────┘ └──────┘
txt └──────────┘ └──────┘
par └──────────┘ └──────┘
pid └──────────┘ └┘
st ┴└────────┘└─
58 change finset.univ.sum (λy:n, (c * M x y) * v y) = _,
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
typ └─────┘└─────────────┘┴ └┘┴└┘ ┴┴ ┴┴┴┴┴ └┘ ┴┴┴ └┘ └┘
doc └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
txt └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
par └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
pid ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘
st ───────────────────────────────────────────────────────┘└─
59 simp only [_root_.mul_assoc, finset.mul_sum.symm],
id └──────────────┘
src └─────────┘└──────────────┘└┘ ┴
typ └─────────┘└──────────────┘└┘└─────────────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ────────────────────────────────────────────────────┘└─
60 refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└┘└
61 { assume M v w, funext x,
src └──────────┘ └──────┘
typ └──────────┘ └──────┘
doc └──────────┘ └──────┘
txt └──────────┘ └──────┘
par └──────────┘ └──────┘
pid └──────────┘ └┘
st ───┘└──────────┘└────────┘└─
62 change finset.univ.sum (λy:n, M x y * (v y + w y)) = _,
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
typ └─────┘└─────────────┘┴ └┘┴└┘┴┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴┴ └─┘ └┘
doc └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
txt └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
par └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
pid ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
st ─────────────────────────────────────────────────────────┘└─
63 simp [_root_.mul_add, finset.sum_add_distrib],
id └────────────┘ └────────────────────┘
src └────┘└────────────┘└┘└────────────────────┘┴
typ └────┘└────────────┘└┘└────────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────────────────────────────┘└─
64 refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└┘└
65 { assume c M v, funext x,
src └──────────┘ └──────┘
typ └──────────┘ └──────┘
doc └──────────┘ └──────┘
txt └──────────┘ └──────┘
par └──────────┘ └──────┘
pid └──────────┘ └┘
st ───────────────┘└────────┘└─
66 change finset.univ.sum (λy:n, M x y * (c * v y)) = _,
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
typ └─────┘└─────────────┘┴ └┘┴└┘┴┴┴┴ ┴ ┴ ┴┴ ┴┴┴ └─┘ └┘
doc └─────┘└─────────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
txt └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
par └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
pid ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
st ───────────────────────────────────────────────────────┘└─
67 rw [show (λy:n, M x y * (c * v y)) = (λy:n, c * (M x y * v y)), { funext n, ac_refl },
id ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└──────┘└──
typ └──┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ └┘┴└┘┴┴ ┴ ┴┴┴┴ ┴ ┴┴┴ └────┘└──────┘└┘└──────┘└──
doc └──┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└──────┘└──
txt └──┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└──────┘└──
par └──┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└──────┘└──
pid └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────────────
st ────────────────────────────────────────────────────────────────────┘└───────┘└────────┘┴└─
68 ← finset.mul_sum],
id └────────────┘
src ───────┘└────────────┘┴
typ ───────┘└────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ─────────────────────┘└──
69 refl }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
70 end
st ──┘
71
72 /-- Evaluation of matrices gives a map from matrix m n R to
73 linear maps (n → R) →ₗ[R] (m → R). -/
74 def to_lin : matrix m n R → (n → R) →ₗ[R] (m → R) := eval.to_fun
id └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └──┘└─────┘
src └────┘ └─┘ ┴ └──┘└─────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └──┘└─────┘
doc └──┘
75
76 lemma to_lin_add (M N : matrix m n R) : (M + N).to_lin = M.to_lin + N.to_lin :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└─────┘ ┴ ┴└─────┘
src └────┘ ┴ └────┘ ┴ └─────┘ ┴ └─────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└─────┘ ┴ ┴└─────┘
doc └────┘ └─────┘ └─────┘
77 matrix.eval.map_add M N
id └─────────┘└──────┘ ┴ ┴
src └─────────┘└──────┘
typ └─────────┘└──────┘ ┴ ┴
doc └─────────┘
78
79 @[simp] lemma to_lin_zero : (0 : matrix m n R).to_lin = 0 :=
id └────┘ ┴ ┴ ┴ └────┘ ┴
src └────┘ └────┘ ┴
typ └────┘ ┴ ┴ ┴ └────┘ ┴
doc └──┘ └────┘
80 matrix.eval.map_zero
id └─────────┘└───────┘
src └─────────┘└───────┘
typ └─────────┘└───────┘
doc └─────────┘
81
82 instance to_lin.is_linear_map :
83 @is_linear_map R (matrix m n R) ((n → R) →ₗ[R] (m → R)) _ _ _ _ _ to_lin :=
id └───────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘
src └───────────┘ └────┘ └─┘ ┴ └────┘
typ └───────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘
doc └────┘
84 matrix.eval.is_linear
id └─────────┘└────────┘
src └─────────┘└────────┘
typ └─────────┘└────────┘
doc └─────────┘
85
86 instance to_lin.is_add_monoid_hom :
87 @is_add_monoid_hom (matrix m n R) ((n → R) →ₗ[R] (m → R)) _ _ to_lin :=
id └───────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘
src └───────────────┘ └────┘ └─┘ ┴ └────┘
typ └───────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘
doc └───────────────┘ └────┘
88 { map_zero := to_lin_zero, map_add := to_lin_add }
id └─────────┘ └────────┘
src └─────────┘ └────────┘
typ └─────────┘ └────────┘
89
90 @[simp] lemma to_lin_apply (M : matrix m n R) (v : n → R) :
id └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
91 (M.to_lin : (n → R) → (m → R)) v = mul_vec M v := rfl
id ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
src └─────┘ ┴ └─────┘ └─┘
typ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
doc └─────┘
92
93 lemma mul_to_lin [decidable_eq l] (M : matrix m n R) (N : matrix n l R) :
id └──────────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └──────────┘ └────┘ └────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
94 (M.mul N).to_lin = M.to_lin.comp N.to_lin :=
id ┴└──┘ ┴ └────┘ ┴ ┴└─────┘└───┘ ┴└─────┘
src └──┘ └────┘ ┴ └─────┘└───┘ └─────┘
typ ┴└──┘ ┴ └────┘ ┴ ┴└─────┘└───┘ ┴└─────┘
doc └────┘ └─────┘ └─────┘
95 begin
st └─────
96 ext v x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └──┘
st ────────┘└─
97 simp [to_lin_apply, mul_vec, matrix.mul, finset.sum_mul, finset.mul_sum],
id └──────────┘ └─────┘ └────────┘ └────────────┘ └────────────┘
src └────┘└──────────┘└┘└─────┘└┘└────────┘└┘└────────────┘└┘└────────────┘┴
typ └────┘└──────────┘└┘└─────┘└┘└────────┘└┘└────────────┘└┘└────────────┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
98 rw [finset.sum_comm],
id └─────────────┘
src └──┘└─────────────┘┴
typ └──┘└─────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────┘└──
99 congr, funext x, congr, funext y,
src └───┘ └──────┘ └───┘ └──────┘
typ └───┘ └──────┘ └───┘ └──────┘
doc └──────┘ └──────┘
txt └───┘ └──────┘ └───┘ └──────┘
par └───┘ └──────┘ └───┘ └──────┘
pid └┘ └┘
st ──────┘└────────┘└─────┘└────────┘└─
100 rw [mul_assoc]
id └───────┘
src └──┘└───────┘└┘
typ └──┘└───────┘└┘
doc └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st ──────────────┘┴┴
101 end
st └─┘
102
103 end matrix
104
105 namespace linear_map
106
107 variables {R : Type v} [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
108
109 /-- The linear map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R. -/
110 def to_matrixₗ [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) →ₗ[R] matrix m n R :=
id └──────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └─┘┴┴ └────┘ ┴ ┴ ┴
src └──────────┘ └─┘ ┴ └─┘ ┴ └────┘
typ └──────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └─┘┴┴ └────┘ ┴ ┴ ┴
111 begin
st └─────
112 refine linear_map.mk (λ f i j, f (λ n, ite (j = n) 1 0) i) _ _,
id └───────────┘ └─┘ ┴
src └─────┘└───────────┘┴ └──────┘ ┴ └──┘└─┘┴ ┴┴┴ └─────┘ └───┘
typ └─────┘└───────────┘┴ └──────┘ ┴ └──┘└─┘┴ ┴┴┴ └─────┘ └───┘
doc └─────┘ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └───┘
txt └─────┘ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └───┘
par └─────┘ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └───┘
pid ┴ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └───┘
st ───────────────────────────────────────────────────────────────┘└─
113 { assume f g, simp only [add_apply], refl },
id └───────┘
src └────────┘ └─────────┘└───────┘┴ └───┘
typ └────────┘ └─────────┘└───────┘┴ └───┘
doc └────────┘ └─────────┘ ┴ └───┘
txt └────────┘ └─────────┘ ┴ └───┘
par └────────┘ └─────────┘ ┴ └───┘
pid └────────┘ ┴└──┘└┘ ┴ ┴
st ───┘└────────┘└─────────────────────┘└─────┘└┘└
114 { assume f g, simp only [smul_apply], refl }
id └────────┘
src └────────┘ └─────────┘└────────┘┴ └───┘
typ └────────┘ └─────────┘└────────┘┴ └───┘
doc └────────┘ └─────────┘ ┴ └───┘
txt └────────┘ └─────────┘ ┴ └───┘
par └────────┘ └─────────┘ ┴ └───┘
pid └────────┘ ┴└──┘└┘ ┴ ┴
st ─────────────┘└──────────────────────┘└─────┘└─
115 end
st ──┘
116
117 /-- The map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R. -/
118 def to_matrix [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) → matrix m n R := to_matrixₗ.to_fun
id └──────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────────┘└─────┘
src └──────────┘ └─┘ ┴ └────┘ └────────┘└─────┘
typ └──────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────────┘└─────┘
doc └────────┘
119
120 end linear_map
121
122 section linear_equiv_matrix
123
124 variables {R : Type v} [comm_ring R] [decidable_eq n]
id ┴ └───────┘ └──────────┘
src └───────┘ └──────────┘
typ ┴ └───────┘ └──────────┘
125
126 open finsupp matrix linear_map
127
128 /-- to_lin is the left inverse of to_matrix. -/
129 lemma to_matrix_to_lin {f : (n → R) →ₗ[R] (m → R)} :
id ┴ ┴ └─┘┴┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ └─┘┴┴ ┴ ┴
130 to_lin (to_matrix f) = f :=
id └────┘ └───────┘ ┴ ┴ ┴
src └────┘ └───────┘ ┴
typ └────┘ └───────┘ ┴ ┴ ┴
doc └────┘ └───────┘
131 begin
st └─────
132 ext : 1,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴└┘┴
st ────────┘└─
133 -- Show that the two sides are equal by showing that they are equal on a basis
st ─────────────────────────────────────────────────────────────────────────────────
134 convert linear_eq_on (set.range _) _ (is_basis.mem_span (@pi.is_basis_fun R n _ _) _),
id └──────────┘ └───────┘ └───────────────┘ └─────────────┘ ┴ ┴
src └──────┘└──────────┘┴ └───────┘└────┘ └───────────────┘┴ └─────────────┘┴ ┴ └──────┘
typ └──────┘└──────────┘┴ └───────┘└────┘ └───────────────┘┴ └─────────────┘┴┴┴┴└──────┘
doc └──────┘ ┴ └───────┘└────┘ ┴ ┴ ┴ └──────┘
txt └──────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘
par └──────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘
pid ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
135 assume e he,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
136 rw [@std_basis_eq_single R _ _ _ 1] at he,
id └─────────────────┘ ┴
src └──┘ └─────────────────┘┴ └─────────────┘
typ └──┘ └─────────────────┘┴┴└─────────────┘
doc └──┘ ┴ └─────────────┘
txt └──┘ ┴ └─────────────┘
par └──┘ ┴ └─────────────┘
pid └┘ ┴ └───────┘└────┘
st ──────────────────────────────────┘└┘└────┘└─
137 cases (set.mem_range.mp he) with i h,
id └──────────────┘ └┘
src └────┘ └──────────────┘┴ └────────┘
typ └────┘ └──────────────┘┴└┘└────────┘
doc └────┘ ┴ └────────┘
txt └────┘ ┴ └────────┘
par └────┘ ┴ └────────┘
pid ┴ ┴ ┴└───────┘
st ─────────────────────────────────────┘└─
138 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
139 change finset.univ.sum (λ k, (f.to_fun (λ l, ite (k = l) 1 0)) j * (e k)) = _,
id └─────────────┘ └──────┘ └─┘ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ └──┘ └──────┘┴ └──┘└─┘┴ ┴┴┴ └──────┘ ┴┴┴ ┴ └─┘ └┘
typ └─────┘└─────────────┘┴ └──┘ └──────┘┴ └──┘└─┘┴ ┴┴┴ └──────┘┴┴┴┴ ┴┴ └─┘ └┘
doc └─────┘└─────────────┘┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─┘ └┘
txt └─────┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─┘ └┘
par └─────┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─┘ └┘
pid ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └─┘ └┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
140 rw [←h],
id ┴
src └───┘ ┴
typ └───┘┴┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ───────┘└──
141 conv_lhs { congr, skip, funext,
src └─────────┘└───┘└┘└──┘└┘└────┘└─
typ └─────────┘└───┘└┘└──┘└┘└────┘└─
txt └─────────┘└───┘└┘└──┘└┘└────┘└─
par └─────────┘└───┘└┘└──┘└┘└────┘└─
pid ┴└──────────────────────
st ───────────┘└────┘└────┘└──────┘└─
142 rw [mul_comm, ←smul_eq_mul, ←pi.smul_apply, ←linear_map.smul],
id └──────┘ └─────────┘ └───────────┘ └─────────────┘
src ───┘└──┘└──────┘└─┘└─────────┘└─┘└───────────┘└─┘└─────────────┘┴└─
typ ───┘└──┘└──────┘└─┘└─────────┘└─┘└───────────┘└─┘└─────────────┘┴└─
txt ───┘└──┘ └─┘ └─┘ └─┘ ┴└─
par ───┘└──┘ └─┘ └─┘ └─┘ ┴└─
pid ───────┘ └─┘ └─┘ └─┘ └──
st ───────────────┘└────────────┘└──────────────┘└────────────────┘ └─
143 rw [show _ = ite (i = k) (1:R) 0, by convert single_apply],
id ┴ └─┘ ┴ ┴ ┴ └──────────┘
src ───┘└──┘ └─┘ ┴└─┘┴ ┴ ┴ └┘ └┘ └──────┘└──────┘└──────────┘┴└─
typ ───┘└──┘ └─┘┴┴└─┘┴ ┴┴ ┴┴└┘ └┘┴└──────┘└──────┘└──────────┘┴└─
doc └──────┘
txt ───┘└──┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘└──────┘ ┴└─
par ───┘└──┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘└──────┘ ┴└─
pid ───────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────────────┘ └──
st ───────────────────────────────────────┘└───────────────────┘ └─
144 rw [show f.to_fun (ite (i = k) (1:R) 0 • (λ l, ite (k = l) 1 0)) = ite (i = k) (f.to_fun _) 0,
id ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘
src ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └──┘┴┴ └──┘ ┴ ┴ ┴ └──────┘ ┴└─┘┴ ┴ ┴ └┘ └──────┘└──────
typ ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘┴└──┘┴┴ └──┘ ┴ ┴ ┴ └──────┘┴┴└─┘┴ ┴┴ ┴┴└┘ └──────┘└──────
txt ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ └──────
par ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ └──────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └──┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ └──────
st ───────────────────────────────────────────────────────────────────────────────────────────────────
145 { split_ifs, { rw [one_smul] }, { rw [zero_smul], exact linear_map.map_zero f } }] },
id └──────┘ └───────┘ └─────────────────┘ ┴
src ───────┘└───────┘└──┘└──┘└──────┘└┘└───┘└──┘└───────┘┴└┘└────┘└─────────────────┘┴ ┴└───┘┴
typ ───────┘└───────┘└──┘└──┘└──────┘└┘└───┘└──┘└───────┘┴└┘└────┘└─────────────────┘┴┴┴└───┘┴
doc └───────┘ └──┘ └┘ └──┘ ┴ └────┘ ┴ ┴
txt ───────┘└───────┘└──────┘ └─────────┘ └─┘└────┘ ┴ ┴└───┘┴
par ───────┘└───────┘└──┘└──┘ └┘└───┘└──┘ ┴└┘└────┘ ┴ ┴└───┘┴
pid ────────────────────────┘ └─────────┘ └───────┘ ┴ └─────┘
st ──────┘└────────┘└─┘└───────────┘┴┴┴└───────────────┘└─────────────────────────────┘└──┘┴└┘└
146 convert finset.sum_eq_single i _ _,
id └──────────────────┘ ┴
src └──────┘└──────────────────┘┴ └──┘
typ └──────┘└──────────────────┘┴┴└──┘
doc └──────┘ ┴ └──┘
txt └──────┘ ┴ └──┘
par └──────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ───────────────────────────────────┘└─
147 { rw [if_pos rfl], convert rfl, ext, congr },
id └────┘ └─┘ └─┘
src └──┘└────┘┴└─┘┴ └──────┘└─┘ └─┘ └────┘
typ └──┘└────┘┴└─┘┴ └──────┘└─┘ └─┘ └────┘
doc └──┘ ┴ ┴ └──────┘ └─┘
txt └──┘ ┴ ┴ └──────┘ └─┘ └────┘
par └──┘ ┴ ┴ └──────┘ └─┘ └────┘
pid └┘ ┴ ┴ ┴ ┴
st ───┘└────────────┘└────────────┘└───┘└──────┘└┘└
148 { assume _ _ hbi, rw [if_neg $ ne.symm hbi], refl },
id └────┘ └─────┘ └─┘
src └────────────┘ └──┘└────┘┴ ┴└─────┘┴ ┴ └───┘
typ └────────────┘ └──┘└────┘┴ ┴└─────┘┴└─┘┴ └───┘
doc └────────────┘ └──┘ ┴ ┴ ┴ ┴ └───┘
txt └────────────┘ └──┘ ┴ ┴ ┴ ┴ └───┘
par └────────────┘ └──┘ ┴ ┴ ┴ ┴ └───┘
pid └────────────┘ └┘ ┴ ┴ ┴ ┴ ┴
st ───┘└────────────┘└────────────────────────┘└──────┘└┘└
149 { assume hi, exact false.elim (hi $ finset.mem_univ i) }
id └────────┘ └┘ └─────────────┘ ┴
src └───────┘ └────┘└────────┘┴ ┴ ┴└─────────────┘┴ └┘
typ └───────┘ └────┘└────────┘┴ └┘┴ ┴└─────────────┘┴┴└┘
doc └───────┘ └────┘ ┴ ┴ ┴ ┴ └┘
txt └───────┘ └────┘ ┴ ┴ ┴ ┴ └┘
par └───────┘ └────┘ ┴ ┴ ┴ ┴ └┘
pid └───────┘ ┴ ┴ ┴ ┴ ┴ ┴┴
st ────────────┘└──────────────────────────────────────────┘└─
150 end
st ──┘
151
152 /-- to_lin is the right inverse of to_matrix. -/
153 lemma to_lin_to_matrix {M : matrix m n R} : to_matrix (to_lin M) = M :=
id └────┘ ┴ ┴ ┴ └───────┘ └────┘ ┴ ┴ ┴
src └────┘ └───────┘ └────┘ ┴
typ └────┘ ┴ ┴ ┴ └───────┘ └────┘ ┴ ┴ ┴
doc └───────┘ └────┘
154 begin
st └─────
155 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
156 change finset.univ.sum (λ y, M i y * ite (j = y) 1 0) = M i j,
id └─────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ └──┘ ┴ ┴ ┴┴┴└─┘┴ ┴┴┴ └─────┘ ┴ ┴ ┴
typ └─────┘└─────────────┘┴ └──┘ ┴ ┴ ┴┴┴└─┘┴ ┴┴┴ └─────┘ ┴┴┴┴┴┴
doc └─────┘└─────────────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
txt └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
par └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
157 have h1 : (λ y, M i y * ite (j = y) 1 0) = (λ y, ite (j = y) (M i y) 0),
id └─┘ ┴ ┴ ┴
src └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘└─┘┴ ┴ ┴ └┘ ┴ ┴ └──┘
typ └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘└─┘┴ ┴┴ ┴ └┘ ┴┴┴┴ └──┘
doc └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
txt └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
par └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
pid └─────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────┘└─
158 { ext, split_ifs, exact mul_one _, exact ring.mul_zero _ },
id └─────┘ └───────────┘
src └─┘ └───────┘ └────┘└─────┘└┘ └────┘└───────────┘└─┘
typ └─┘ └───────┘ └────┘└─────┘└┘ └────┘└───────────┘└─┘
doc └─┘ └───────┘ └────┘ └┘ └────┘ └─┘
txt └─┘ └───────┘ └────┘ └┘ └────┘ └─┘
par └─┘ └───────┘ └────┘ └┘ └────┘ └─┘
pid ┴ └┘ ┴ └┘┴
st ─────┘└─┘└─────────┘└───────────────┘└──────────────────────┘└┘└
159 have h2 : finset.univ.sum (λ y, ite (j = y) (M i y) 0) = (finset.singleton j).sum (λ y, ite (j = y) (M i y) 0),
id └─────────────┘ └──────────────┘ └─┘ ┴ ┴ ┴
src └────────┘└─────────────┘┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ └──────────────┘┴ └────┘ └──┘└─┘┴ ┴ ┴ └┘ ┴ ┴ └──┘
typ └────────┘└─────────────┘┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ └──────────────┘┴ └────┘ └──┘└─┘┴ ┴┴ ┴ └┘ ┴┴┴┴ └──┘
doc └────────┘└─────────────┘┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ └──────────────┘┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
txt └────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
par └────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
pid └─────┘└─┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
160 { refine (finset.sum_subset _ _).symm,
id └───────────────┘
src └─────┘ └───────────────┘└────────┘
typ └─────┘ └───────────────┘└────────┘
doc └─────┘ └────────┘
txt └─────┘ └────────┘
par └─────┘ └────────┘
pid ┴ └───────┘┴
st ─────┘└─────────────────────────────────┘└─
161 { intros _ H, rwa finset.mem_singleton.1 H, exact finset.mem_univ _ },
id └──────────────────┘ ┴ └─────────────┘
src └────────┘ └──┘└──────────────────┘└─┘ └────┘└─────────────┘└─┘
typ └────────┘ └──┘└──────────────────┘└─┘┴ └────┘└─────────────┘└─┘
doc └────────┘ └──┘ └─┘ └────┘ └─┘
txt └────────┘ └──┘ └─┘ └────┘ └─┘
par └────────┘ └──┘ └─┘ └────┘ └─┘
pid └──┘ ┴ └─┘ ┴ └┘┴
st ───────┘└────────┘└────────────────────────────┘└────────────────────────┘└┘└
162 { exact λ _ _ H, if_neg (mt (finset.mem_singleton.2 ∘ eq.symm) H) } },
id └────┘ └┘ └──────────────────┘ ┴ └─────┘
src └────┘ └──────┘└────┘┴ └┘┴ └──────────────────┘└─┘┴┴└─────┘└┘ └┘
typ └────┘ └──────┘└────┘┴ └┘┴ └──────────────────┘└─┘┴┴└─────┘└┘ └┘
doc └────┘ └──────┘ ┴ ┴ └─┘ ┴ └┘ └┘
txt └────┘ └──────┘ ┴ ┴ └─┘ ┴ └┘ └┘
par └────┘ └──────┘ ┴ ┴ └─┘ ┴ └┘ └┘
pid ┴ └──────┘ ┴ ┴ └─┘ ┴ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────┘└──┘└
163 rw [h1, h2, finset.sum_singleton],
id └┘ └┘ └──────────────────┘
src └──┘ └┘ └┘└──────────────────┘┴
typ └──┘└┘└┘└┘└┘└──────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────┘└──┘└────────────────────┘└──
164 exact if_pos rfl
id └────┘ └─┘
src └────┘└────┘┴└─┘┴
typ └────┘└────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────┘
165 end
st └─┘
166
167 /-- Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R. -/
168 def linear_equiv_matrix' : ((n → R) →ₗ[R] (m → R)) ≃ₗ[R] matrix m n R :=
id ┴ ┴ └─┘┴┴ ┴ ┴ └─┘┴┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └────┘
typ ┴ ┴ └─┘┴┴ ┴ ┴ └─┘┴┴ └────┘ ┴ ┴ ┴
doc └─┘ ┴
169 { to_fun := to_matrix,
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
170 inv_fun := to_lin,
id └────┘
src └────┘
typ └────┘
doc └────┘
171 right_inv := λ _, to_lin_to_matrix,
id ┴ └──────────────┘
src └──────────────┘
typ ┴ └──────────────┘
doc └──────────────┘
172 left_inv := λ _, to_matrix_to_lin,
id ┴ └──────────────┘
src └──────────────┘
typ ┴ └──────────────┘
doc └──────────────┘
173 add := to_matrixₗ.add,
id └────────┘└──┘
src └────────┘└──┘
typ └────────┘└──┘
doc └────────┘
174 smul := to_matrixₗ.smul }
id └────────┘└───┘
src └────────┘└───┘
typ └────────┘└───┘
doc └────────┘
175
176 /-- Given a basis of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence
177 between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases. -/
178 def linear_equiv_matrix {ι κ M₁ M₂ : Type*}
179 [add_comm_group M₁] [module R M₁]
id └────────────┘ └┘ └────┘ ┴ └┘
src └────────────┘ └────┘
typ └────────────┘ └┘ └────┘ ┴ └┘
doc └────┘
180 [add_comm_group M₂] [module R M₂]
id └────────────┘ └┘ └────┘ ┴ └┘
src └────────────┘ └────┘
typ └────────────┘ └┘ └────┘ ┴ └┘
doc └────┘
181 [fintype ι] [decidable_eq ι] [fintype κ] [decidable_eq κ]
id └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘ └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘ └─────┘
182 {v₁ : ι → M₁} {v₂ : κ → M₂} (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) :
id ┴ └┘ ┴ └┘ └──────┘ ┴ └┘ └──────┘ ┴ └┘
src └──────┘ └──────┘
typ ┴ └┘ ┴ └┘ └──────┘ ┴ └┘ └──────┘ ┴ └┘
doc └──────┘ └──────┘
183 (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix κ ι R :=
id └┘ └─┘┴┴ └┘ └─┘┴┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └────┘
typ └┘ └─┘┴┴ └┘ └─┘┴┴ └────┘ ┴ ┴ ┴
doc └─┘ ┴
184 linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) linear_equiv_matrix'
id └────────────────┘ └──────────────────────┘ └─────────────┘ └─┘ └─────────────┘ └─┘ └──────────────────┘
src └────────────────┘ └──────────────────────┘ └─────────────┘ └─────────────┘ └──────────────────┘
typ └────────────────┘ └──────────────────────┘ └─────────────┘ └─┘ └─────────────┘ └─┘ └──────────────────┘
doc └────────────────┘ └──────────────────────┘ └─────────────┘ └─────────────┘ └──────────────────┘
185
186 end linear_equiv_matrix
187
188 namespace matrix
189 open_locale matrix
190
191 section trace
192
193 variables {R : Type v} {M : Type w} [ring R] [add_comm_group M] [module R M]
id └──┘ └────────────┘ └────┘
src └──┘ └────────────┘ └────┘
typ └──┘ └────────────┘ └────┘
doc └────┘
194
195 /--
196 The diagonal of a square matrix.
197 -/
198 def diag (n : Type u) (R : Type v) (M : Type w)
199 [ring R] [add_comm_group M] [module R M] [fintype n] : (matrix n n M) →ₗ[R] n → M := {
id └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
src └──┘ └────────────┘ └────┘ └─────┘ └────┘ └─┘ ┴
typ └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
doc └────┘ └─────┘
200 to_fun := λ A i, A i i,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
201 add := by { intros, ext, refl, },
src └────┘ └─┘ └──┘
typ └────┘ └─┘ └──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
st └───────┘└───┘└────┘└──┘
202 smul := by { intros, ext, refl, } }
src └────┘ └─┘ └──┘
typ └────┘ └─┘ └──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
st └───────┘└───┘└────┘└──┘
203
204 @[simp] lemma diag_one [decidable_eq n] :
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──┘
205 diag n R R 1 = λ i, 1 := by { dunfold diag, ext, simp [one_val_eq] }
id └──┘ ┴ ┴ ┴ ┴ ┴ └────────┘
src └──┘ ┴ └──────────┘ └─┘ └────┘└────────┘└┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ └─┘ └────┘└────────┘└┘
doc └──┘ └──────────┘ └─┘ └────┘ └┘
txt └──────────┘ └─┘ └────┘ └┘
par └──────────┘ └─┘ └────┘ └┘
pid └───┘ ┴┴ ┴┴
st └─────────────┘└───┘└──────────────────┘└┘
206
207 @[simp] lemma diag_transpose (A : matrix n n M) : diag n R M Aᵀ = diag n R M A := rfl
id └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
src └────┘ └──┘ ┴ ┴ └──┘ └─┘
typ └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └──┘ └──┘
208
209 /--
210 The trace of a square matrix.
211 -/
212 def trace (n : Type u) (R : Type v) (M : Type w)
213 [ring R] [add_comm_group M] [module R M] [fintype n] : (matrix n n M) →ₗ[R] M := {
id └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └──┘ └────────────┘ └────┘ └─────┘ └────┘ └─┘ ┴
typ └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └────┘ └─────┘
214 to_fun := finset.univ.sum ∘ (diag n R M),
id └─────────┘└──┘ ┴ └──┘ ┴ ┴ ┴
src └─────────┘└──┘ ┴ └──┘
typ └─────────┘└──┘ ┴ └──┘ ┴ ┴ ┴
doc └─────────┘ └──┘
215 add := by { intros, apply finset.sum_add_distrib, },
id └────────────────────┘
src └────┘ └────┘└────────────────────┘
typ └────┘ └────┘└────────────────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴
st └───────┘└────────────────────────────┘└──┘
216 smul := by { intros, simp [finset.smul_sum], } }
id └─────────────┘
src └────┘ └────┘└─────────────┘┴
typ └────┘ └────┘└─────────────┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴┴ ┴
st └───────┘└──────────────────────┘└──┘
217
218 @[simp] lemma trace_one [decidable_eq n] :
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──┘
219 trace n R R 1 = fintype.card n :=
id └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
src └───┘ ┴ └──────────┘
typ └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └───┘ └──────────┘
220 have h : trace n R R 1 = finset.univ.sum (diag n R R 1) := rfl,
id └───┘ ┴ ┴ ┴ ┴ └─────────┘└──┘ └──┘ ┴ ┴ ┴ └─┘
src └───┘ ┴ └─────────┘└──┘ └──┘ └─┘
typ └───┘ ┴ ┴ ┴ ┴ └─────────┘└──┘ └──┘ ┴ ┴ ┴ └─┘
doc └───┘ └─────────┘ └──┘
221 by rw [h, diag_one, finset.sum_const, add_monoid.smul_one]; refl
id ┴ └──────┘ └──────────────┘ └─────────────────┘
src └──┘ └┘└──────┘└┘└──────────────┘└┘└─────────────────┘┴ └────
typ └──┘┴└┘└──────┘└┘└──────────────┘└┘└─────────────────┘┴ └────
doc └──┘ └┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ ┴ └
st └────┘└────────┘└────────────────┘└───────────────────┘┴└──────
222
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
223 @[simp] lemma trace_transpose (A : matrix n n M) : trace n R M Aᵀ = trace n R M A := rfl
id └────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘
src └────┘ └───┘ ┴ ┴ └───┘ └─┘
typ └────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───┘ └───┘
224
225 @[simp] lemma trace_transpose_mul [decidable_eq n] (A : matrix m n R) (B : matrix n m R) :
id └──────────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └──────────┘ └────┘ └────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └──┘
226 trace n R R (Aᵀ ⬝ Bᵀ) = trace m R R (A ⬝ B) := finset.sum_comm
id └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘
src └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─────────────┘
typ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘
doc └───┘ └───┘
227
228 lemma trace_mul_comm {S : Type v} [comm_ring S] [decidable_eq n]
id └───────┘ ┴ └──────────┘ ┴
src └───────┘ └──────────┘
typ └───────┘ ┴ └──────────┘ ┴
229 (A : matrix m n S) (B : matrix n m S) :
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ └────┘
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
230 trace n S S (B ⬝ A) = trace m S S (A ⬝ B) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
231 by rw [←trace_transpose, ←trace_transpose_mul, transpose_mul]
id └─────────────┘ └─────────────────┘ └───────────┘
src └───┘└─────────────┘└─┘└─────────────────┘└┘└───────────┘└─
typ └───┘└─────────────┘└─┘└─────────────────┘└┘└───────────┘└─
doc └───┘ └─┘ └┘ └─
txt └───┘ └─┘ └┘ └─
par └───┘ └─┘ └┘ └─
pid └─┘ └─┘ └┘ ┴└
st └───────────────────┘└────────────────────┘└─────────────┘┴└
232
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
233 end trace
234
235 section ring
236
237 variables {R : Type v} [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
238 open linear_map matrix
239
240 lemma proj_diagonal [decidable_eq m] (i : m) (w : m → R) :
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴
241 (proj i).comp (to_lin (diagonal w)) = (w i) • proj i :=
id └──┘ ┴ └──┘ └────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └──┘ └──┘ └────┘ └──────┘ ┴ ┴ └──┘
typ └──┘ ┴ └──┘ └────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘ └────┘ └──┘
242 by ext j; simp [mul_vec_diagonal]
id └──────────────┘
src └───┘ └────┘└──────────────┘└─
typ └───┘ └────┘└──────────────┘└─
doc └───┘ └────┘ └─
txt └───┘ └────┘ └─
par └───┘ └────┘ └─
pid └┘ ┴┴ ┴└
st └───────────────────────────────
243
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
244 lemma diagonal_comp_std_basis [decidable_eq n] (w : n → R) (i : n) :
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴
245 (diagonal w).to_lin.comp (std_basis R (λ_:n, R) i) = (w i) • std_basis R (λ_:n, R) i :=
id └──────┘ ┴ └────┘ └──┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └──────┘ └────┘ └──┘ └───────┘ ┴ ┴ └───────┘
typ └──────┘ ┴ └────┘ └──┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └────┘ └───────┘ └───────┘
246 begin
st └─────
247 ext a j,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └──┘
st ────────┘└─
248 simp only [linear_map.comp_apply, smul_apply, to_lin_apply, mul_vec_diagonal, smul_apply,
id └───────────────────┘ └────────┘ └──────────┘ └──────────────┘ └────────┘
src └─────────┘└───────────────────┘└┘└────────┘└┘└──────────┘└┘└──────────────┘└┘└────────┘└─
typ └─────────┘└───────────────────┘└┘└────────┘└┘└──────────┘└┘└──────────────┘└┘└────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────
249 pi.smul_apply, smul_eq_mul],
id └───────────┘ └─────────┘
src ───┘└───────────┘└┘└─────────┘┴
typ ───┘└───────────┘└┘└─────────┘┴
doc ───┘ └┘ ┴
txt ───┘ └┘ ┴
par ───┘ └┘ ┴
pid ───┘ └┘ ┴
st ──────────────────────────────┘└─
250 by_cases i = j,
id ┴ ┴ ┴
src └───────┘ ┴┴┴
typ └───────┘┴┴┴┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────┘└─
251 { subst h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
252 { rw [std_basis_ne R (λ_:n, R) _ _ (ne.symm h), _root_.mul_zero, _root_.mul_zero] }
id └──────────┘ ┴ ┴ └─────┘ ┴ └─────────────┘ └─────────────┘
src └──┘└──────────┘┴ ┴ └┘ └┘ └────┘ └─────┘┴ └─┘└─────────────┘└┘└─────────────┘└┘
typ └──┘└──────────┘┴ ┴ └┘┴└┘┴└────┘ └─────┘┴┴└─┘└─────────────┘└┘└─────────────┘└┘
doc └──┘ ┴ ┴ └┘ └┘ └────┘ ┴ └─┘ └┘ └┘
txt └──┘ ┴ ┴ └┘ └┘ └────┘ ┴ └─┘ └┘ └┘
par └──┘ ┴ ┴ └┘ └┘ └────┘ ┴ └─┘ └┘ └┘
pid └┘ ┴ ┴ └┘ └┘ └────┘ ┴ └─┘ └┘ ┴┴
st ───────────────────────────────────────────────┘└───────────────┘└───────────────┘┴┴└─
253 end
st ──┘
254
255 end ring
256
257 section vector_space
258
259 variables {K : Type u} [discrete_field K] -- maybe try to relax the universe constraint
id └────────────┘
src └────────────┘
typ └────────────┘
260
261 open linear_map matrix
262
263 lemma rank_vec_mul_vec [decidable_eq n] (w : m → K) (v : n → K) :
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
264 rank (vec_mul_vec w v).to_lin ≤ 1 :=
id └──┘ └─────────┘ ┴ ┴ └────┘ ┴
src └──┘ └─────────┘ └────┘ ┴
typ └──┘ └─────────┘ ┴ ┴ └────┘ ┴
doc └────┘
265 begin
st └─────
266 rw [vec_mul_vec_eq, mul_to_lin],
id └────────────┘ └────────┘
src └──┘└────────────┘└┘└────────┘┴
typ └──┘└────────────┘└┘└────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────┘└──────────┘└──
267 refine le_trans (rank_comp_le1 _ _) _,
id └──────┘ └───────────┘
src └─────┘└──────┘┴ └───────────┘└─────┘
typ └─────┘└──────┘┴ └───────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────────────────┘└─
268 refine le_trans (rank_le_domain _) _,
id └──────┘ └────────────┘
src └─────┘└──────┘┴ └────────────┘└───┘
typ └─────┘└──────┘┴ └────────────┘└───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────────────────┘└─
269 rw [dim_fun', ← cardinal.fintype_card],
id └──────┘ └───────────────────┘
src └──┘└──────┘└──┘└───────────────────┘┴
typ └──┘└──────┘└──┘└───────────────────┘┴
doc └──┘ └──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ─────────────┘└───────────────────────┘└──
270 exact le_refl _
id └─────┘
src └────┘└─────┘└─┘
typ └────┘└─────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────┘
271 end
st └─┘
272
273 set_option class.instance_max_depth 100
doc └──────────────────────┘
274
275 lemma diagonal_to_lin [decidable_eq m] (w : m → K) :
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
276 (diagonal w).to_lin = linear_map.pi (λi, w i • linear_map.proj i) :=
id └──────┘ ┴ └────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴
src └──────┘ └────┘ ┴ └───────────┘ ┴ └─────────────┘
typ └──────┘ ┴ └────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴
doc └────┘ └───────────┘ └─────────────┘
277 by ext v j; simp [mul_vec_diagonal]
id └──────────────┘
src └─────┘ └────┘└──────────────┘└─
typ └─────┘ └────┘└──────────────┘└─
doc └─────┘ └────┘ └─
txt └─────┘ └────┘ └─
par └─────┘ └────┘ └─
pid └──┘ ┴┴ ┴└
st └─────────────────────────────────
278
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
279 lemma ker_diagonal_to_lin [decidable_eq m] (w : m → K) :
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
280 ker (diagonal w).to_lin = (⨆i∈{i | w i = 0 }, range (std_basis K (λi, K) i)) :=
id └─┘ └──────┘ ┴ └────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └───┘ └───────┘ ┴ ┴ ┴ ┴
src └─┘ └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └───────┘
typ └─┘ └──────┘ ┴ └────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └───┘ └───────┘ ┴ ┴ ┴ ┴
doc └─┘ └────┘ ┴ ┴ └───┘ └───────┘
281 begin
st └─────
282 rw [← comap_bot, ← infi_ker_proj],
id └───────┘ └───────────┘
src └────┘└───────┘└──┘└───────────┘┴
typ └────┘└───────┘└──┘└───────────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ────────────────┘└───────────────┘└──
283 simp only [comap_infi, (ker_comp _ _).symm, proj_diagonal, ker_smul'],
id └────────┘ └──────┘ └───────────┘ └───────┘
src └─────────┘└────────┘└┘ └──────┘└──────────┘└───────────┘└┘└───────┘┴
typ └─────────┘└────────┘└┘ └──────┘└──────────┘└───────────┘└┘└───────┘┴
doc └─────────┘ └┘ └──────────┘ └┘ ┴
txt └─────────┘ └┘ └──────────┘ └┘ ┴
par └─────────┘ └┘ └──────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ └──────────┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
284 have : univ ⊆ {i : m | w i = 0} ∪ -{i : m | w i = 0}, { rw set.union_compl_self },
id └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └──────────────────┘
src └─────┘└──┘┴┴┴ └──┘ └─┘ ┴ ┴┴└──┘┴┴┴┴└──┘ └─┘ ┴ ┴ └─┘ └─┘└──────────────────┘┴
typ └─────┘└──┘┴┴┴ └──┘ └─┘ ┴ ┴┴└──┘┴┴┴┴└──┘┴└─┘┴┴ ┴ └─┘ └─┘└──────────────────┘┴
doc └─────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
txt └─────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
par └─────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
pid └───┘└┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────┘└──┘└──────────────────────┘└┘└
285 exact (supr_range_std_basis_eq_infi_ker_proj K (λi:m, K)
id └───────────────────────────────────┘ ┴ ┴
src └────┘ └───────────────────────────────────┘┴ ┴ └┘ └┘ └─
typ └────┘ └───────────────────────────────────┘┴ ┴ └┘┴└┘┴└─
doc └────┘ ┴ ┴ └┘ └┘ └─
txt └────┘ ┴ ┴ └┘ └┘ └─
par └────┘ ┴ ┴ └┘ └┘ └─
pid ┴ ┴ ┴ └┘ └┘ └─
st ───────────────────────────────────────────────────────────
286 (disjoint_compl {i | w i = 0}) this (finite.of_fintype _)).symm
id └────────────┘ ┴ └──┘ └───────────────┘
src ───┘ └────────────┘┴ └──┘ ┴ ┴ └───┘ ┴ └───────────────┘└────────┘
typ ───┘ └────────────┘┴ └──┘┴┴ ┴ └───┘└──┘┴ └───────────────┘└────────┘
doc ───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └────────┘
txt ───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └────────┘
par ───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └────────┘
pid ───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └──────┘└┘
st ───────────────────────────────────────────────────────────────────┘
287 end
st └─┘
288
289 lemma range_diagonal [decidable_eq m] (w : m → K) :
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
290 (diagonal w).to_lin.range = (⨆ i ∈ {i | w i ≠ 0}, (std_basis K (λi, K) i).range) :=
id └──────┘ ┴ └────┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘
src └──────┘ └────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └───┘
typ └──────┘ ┴ └────┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘
doc └────┘ └───┘ ┴ ┴ └───────┘ └───┘
291 begin
st └─────
292 dsimp only [mem_set_of_eq],
id └───────────┘
src └──────────┘└───────────┘┴
typ └──────────┘└───────────┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid └───┘└┘ ┴
st ───────────────────────────┘└─
293 rw [← map_top, ← supr_range_std_basis, map_supr],
id └─────┘ └──────────────────┘ └──────┘
src └────┘└─────┘└──┘└──────────────────┘└┘└──────┘┴
typ └────┘└─────┘└──┘└──────────────────┘└┘└──────┘┴
doc └────┘ └──┘ └┘ ┴
txt └────┘ └──┘ └┘ ┴
par └────┘ └──┘ └┘ ┴
pid └──┘ └──┘ └┘ ┴
st ──────────────┘└──────────────────────┘└────────┘└──
294 congr, funext i,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘
st ──────┘└────────┘└─
295 rw [← linear_map.range_comp, diagonal_comp_std_basis, range_smul'],
id └───────────────────┘ └─────────────────────┘ └─────────┘
src └────┘└───────────────────┘└┘└─────────────────────┘└┘└─────────┘┴
typ └────┘└───────────────────┘└┘└─────────────────────┘└┘└─────────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ────────────────────────────┘└───────────────────────┘└───────────┘└──
296 end
st ──┘
297
298 lemma rank_diagonal [decidable_eq m] (w : m → K) :
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
299 rank (diagonal w).to_lin = fintype.card { i // w i ≠ 0 } :=
id └──┘ └──────┘ ┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └──────┘ └────┘ ┴ └──────────┘ ┴ ┴
typ └──┘ └──────┘ ┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └──────────┘
300 begin
st └─────
301 have hu : univ ⊆ - {i : m | w i = 0} ∪ {i : m | w i = 0}, { rw set.compl_union_self },
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘
src └────────┘└──┘┴┴┴┴┴ └──┘ └─┘ ┴ ┴┴└──┘┴┴┴└──┘ └─┘ ┴ ┴ └─┘ └─┘└──────────────────┘┴
typ └────────┘└──┘┴┴┴┴┴ └──┘ └─┘ ┴ ┴┴└──┘┴┴┴└──┘┴└─┘┴┴ ┴ └─┘ └─┘└──────────────────┘┴
doc └────────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
txt └────────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
par └────────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
pid └─────┘└─┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────────┘└──┘└──────────────────────┘└┘└
302 have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := (disjoint_compl {i | w i = 0}).symm,
id └──────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴
src └────────┘└──────┘┴ └──┘ └─┘ ┴ ┴┴└──┘┴└──┘ └─┘ ┴ ┴ └─────┘ └────────────┘┴ └──┘ ┴ ┴ └───────┘
typ └────────┘└──────┘┴ └──┘ └─┘ ┴ ┴┴└──┘┴└──┘┴└─┘┴┴ ┴ └─────┘ └────────────┘┴ └──┘┴┴ ┴ └───────┘
doc └────────┘└──────┘┴ └──┘ └─┘ ┴ ┴ └──┘ └──┘ └─┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ └───────┘
txt └────────┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ └──┘ └─┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ └───────┘
par └────────┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ └──┘ └─┘ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ └───────┘
pid └─────┘└─┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ └──┘ └─┘ ┴ ┴ └─┘└──┘ ┴ └──┘ ┴ ┴ └──────┘┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
303 have h₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (finite.of_fintype _),
id └───────────────────────────────────┘ ┴ ┴ └┘ └┘ └───────────────┘
src └─────────┘└───────────────────────────────────┘┴ ┴ └┘ └┘ └┘ ┴ ┴ └───────────────┘└─┘
typ └─────────┘└───────────────────────────────────┘┴ ┴ └┘┴└┘┴└┘└┘┴└┘┴ └───────────────┘└─┘
doc └─────────┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └─┘
txt └─────────┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └─┘
par └─────────┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └─┘
pid └─────┘┴└─┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
304 have h₂ := @infi_ker_proj_equiv K _ _ (λi:m, K) _ _ _ _ (by simp; apply_instance) hd hu,
id └─────────────────┘ ┴ ┴ └┘ └┘
src └─────────┘ └─────────────────┘┴ └───┘ └┘ └┘ └────────┘ ┴└──┘└┘└────────────┘└┘ ┴
typ └─────────┘ └─────────────────┘┴ └───┘ └┘┴└┘┴└────────┘ ┴└──┘└┘└────────────┘└┘└┘┴└┘
doc └─────────┘ └─────────────────┘┴ └───┘ └┘ └┘ └────────┘ ┴└──┘└┘└────────────┘└┘ ┴
txt └─────────┘ ┴ └───┘ └┘ └┘ └────────┘ ┴└──┘└┘└────────────┘└┘ ┴
par └─────────┘ ┴ └───┘ └┘ └┘ └────────┘ ┴└──┘└┘└────────────┘└┘ ┴
pid └─────┘┴└─┘ ┴ └───┘ └┘ └┘ └────────┘ └─────────────────────┘ ┴
st ────────────────────────────────────────────────────────────┘└───────────────────┘└─────┘└─
305 rw [rank, range_diagonal, h₁, ←@dim_fun' K],
id └──┘ └────────────┘ └┘ └──────┘ ┴
src └──┘└──┘└┘└────────────┘└┘ └─┘ └──────┘┴ ┴
typ └──┘└──┘└┘└────────────┘└┘└┘└─┘ └──────┘┴┴┴
doc └──┘ └┘ └┘ └─┘ ┴ ┴
txt └──┘ └┘ └┘ └─┘ ┴ ┴
par └──┘ └┘ └┘ └─┘ ┴ ┴
pid └┘ └┘ └┘ └─┘ ┴ ┴
st ─────────┘└──────────────┘└──┘└────────────┘└──
306 apply linear_equiv.dim_eq,
id └─────────────────┘
src └────┘└─────────────────┘
typ └────┘└─────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
307 apply h₂,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└─
308 end
st ──┘
309
310 end vector_space
311
312 end matrix